package alloy.api;

import java.io.BufferedReader;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.FileReader;
import java.io.IOException;
import java.io.PrintStream;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.Collections;
import java.util.Iterator;
import java.util.List;
import java.util.Set;
import java.util.Vector;

import alloy.ast.Command;
import alloy.ast.Formula;
import alloy.util.EnvFailureException;
import alloy.util.Params;
import alloy.viz.alloyviz.VizInstance;

public class AlloyController {

    public static final RunStatus AVAILABLE = new RunStatus();
    public static final RunStatus BUILD_IN_PROGRESS = new RunStatus();
    public static final RunStatus SOLVE_IN_PROGRESS = new RunStatus();
    public static final RunStatus UNSATCORE_IN_PROGRESS = new RunStatus();
    public static final RunStatus COUNT_IN_PROGRESS = new RunStatus();
    public static final RunStatus METAMODEL_IN_PROGRESS = new RunStatus();

    private String spec;
    private SolutionData solutionData;
    private RunStatus runStatus;
    private int commandIndex; // 0 means none selected
    private List commandList;
    private File file;
    private boolean canEnumerate; // if last execution used enumerating solver
    private int solutionCount;
    private Command.Info lastExecutedCommandInfo; // reset to null after build or count
    private boolean isAborting;
    private boolean lastRunAborted;

    // for use with metamodel
    private VizInstance metaInstance;

    // for use with unsat core
    private LiftedUnsatCore liftedUnsatCore;

    // cached formula
    private Formula formulaToAnalyze;

    public AlloyController(File file_) throws FileNotFoundException, IOException {
        BufferedReader reader = new BufferedReader(new FileReader(file_));
        String line;

        spec = "";
        line = reader.readLine();
        while (line != null) {
            spec = spec + line + "\n";
            line = reader.readLine();
        }

        runStatus = AVAILABLE;
        commandIndex = 0;
        file = file_;
        canEnumerate = false;
        solutionCount = 0;
	isAborting = false;
	lastRunAborted = false;
    }

    public AlloyController(String spec_) {
        spec = spec_;
        runStatus = AVAILABLE;
        commandIndex = 0;
        file = null;
        canEnumerate = false;
        solutionCount = 0;
	isAborting = false;
	lastRunAborted = false;
    }

    // passes Boolean.TRUE to finisher if build succeeds, else Boolean.FALSE
    public void build(final ThreadFinisher finisher) throws UnavailableOperationException {
	synchronized(runStatus) {
	    if (!isBuildAvailable())
		throw (new UnavailableOperationException());

	    runStatus = BUILD_IN_PROGRESS;
	}

		AlloyRunner.clearState();
	
        Runnable buildRun = new Runnable() {
            public void run() {
                boolean buildOK;
                if (file == null) {
                    buildOK = AlloyRunner.prepareSpecString(spec);
                }
                else {
                    buildOK = AlloyRunner.prepareSpec(file.getPath());
                }
                

		synchronized(runStatus) {
		    lastRunAborted = isAborting;

		    if (isAborting) {
			buildOK = false;
			isAborting = false;
		    }

		    if (buildOK) {
			Iterator i = AlloyRunner.getCommands().getCommandIter();
			commandList = new Vector();
			while (i.hasNext()) {
			    commandList.add(i.next());
			}
			if (commandList.isEmpty()) {
			    commandIndex = 0;
			}
			else {
			    commandIndex = 1;
			}
		    }
		    else {
			commandList = null;
			commandIndex = 0;
		    }
		    
		    solutionData = null;
		    solutionCount = 0;
		    lastExecutedCommandInfo = null;
		    
		    runStatus = AVAILABLE;
		}

                finisher.threadFinished(new Boolean(buildOK));
            }
        };

        new Thread(buildRun).start();
    }

    // passes Boolean.TRUE to finisher if execution completes, else Boolean.FALSE
    public void execute(final ThreadFinisher finisher) throws UnavailableOperationException {
        execute(null, finisher);
    }


    public void execute(final Set primaryRelations, final ThreadFinisher finisher)
        throws UnavailableOperationException {
	synchronized(runStatus) {
	    if (!isExecuteAvailable(primaryRelations != null))
		throw (new UnavailableOperationException());

	    runStatus = SOLVE_IN_PROGRESS;
	}

        Runnable solveRun = new Runnable() {
            public void run() {
                final Command command = getCommand(); //(Command)commandList.get(commandIndex - 1);
                SolutionData commandData;
                SolutionData newSolutionData = null;
                boolean solveOK = true;

                try {
                    commandData = AlloyRunner.translateCommand(command);
		    if (!isAborting) {
			formulaToAnalyze = commandData.getFormula();
			newSolutionData =
			    AlloyRunner.analyzeCommand(
						       commandData,
						       System.currentTimeMillis(),
						       primaryRelations);
		    }
                }
                catch (TranslationException e) {
                    solveOK = false;
                }
                catch (EnvFailureException efe) {
                         solveOK = false;
                }

		synchronized(runStatus) {
		    lastRunAborted = isAborting;

		    if (isAborting) {
			solveOK = false;
			isAborting = false;
		    }

		    if (solveOK) {
			solutionData = newSolutionData;
			solutionCount = 1;
			lastExecutedCommandInfo = command.info();

			canEnumerate =
			    AlloyRunner.canEnumerateSolutions(Params.glob.getParam("MAIN", "solver"));
		    }
		    else {
			solutionData = null;
			solutionCount = 0;
			lastExecutedCommandInfo = null;
			canEnumerate = false;
		    }
		    
		    runStatus = AVAILABLE;
		}

                finisher.threadFinished(new Boolean(solveOK));
            }
        };

        new Thread(solveRun).start();
    }

    public VizInstance getMetaInstance() {
        return metaInstance;
    }

    public void metamodel(final ThreadFinisher finisher) throws UnavailableOperationException {
	synchronized(runStatus) {
	    if (!isMetamodelAvailable())
		throw (new UnavailableOperationException());

	    runStatus = METAMODEL_IN_PROGRESS;
	}

        Runnable metaRun = new Runnable() {
            public void run() {

                metaInstance = AlloyRunner.metamodel();
                //System.out.println("MetaInstance generated!!!!!!!!!!!!");
                //System.out.println(metaInstance);

		synchronized(runStatus) {
		    lastRunAborted = isAborting;

		    if (isAborting) {
			isAborting = false;
		    }

		    runStatus = AVAILABLE;
		}

                finisher.threadFinished(new Boolean(metaInstance != null));
            }
        };

        new Thread(metaRun).start();
    }

    // passes Boolean.TRUE to finisher if execution completes else Boolean.FALSE
    public void unsatCore(final ThreadFinisher finisher) throws UnavailableOperationException {
	synchronized(runStatus) {
	    if (!isUnsatCoreAvailable()) {
		throw (new UnavailableOperationException());
	    }
	    
	    runStatus = SOLVE_IN_PROGRESS;
	}
	
	Runnable unsatCoreRun = new Runnable() {
		public void run() {
		    boolean unsatCoreOK = true;
		    
		    liftedUnsatCore = AlloyRunner.computeLiftedUnsatCore();

		    synchronized(runStatus) {
			lastRunAborted = isAborting;

			if (isAborting) {
			    unsatCoreOK = false;
			    isAborting = false;
			}

			runStatus = AVAILABLE;
		    }

		    finisher.threadFinished(new Boolean(unsatCoreOK));
		}
	    };
	new Thread(unsatCoreRun).start();
    }

    // passes Boolean.TRUE to finisher if execution completes, else Boolean.FALSE
    public void next(final ThreadFinisher finisher) throws UnavailableOperationException {
	synchronized(runStatus) {
	    if (!isNextAvailable())
		throw (new UnavailableOperationException());
	    
	    runStatus = SOLVE_IN_PROGRESS;
	}

        Runnable nextRun = new Runnable() {
            public void run() {
                SolutionData newSolutionData = null;
                boolean solveOK = true;

                newSolutionData = AlloyRunner.getNextSolution();

		synchronized(runStatus) {
		    lastRunAborted = isAborting;

		    if (isAborting) {
			solveOK = false;
			isAborting = false;
		    }

		    if (solveOK) {
			solutionData = newSolutionData;
			solutionCount++;
		    }
		    
		    runStatus = AVAILABLE;
		}

                finisher.threadFinished(new Boolean(solveOK));
            }
        };

        new Thread(nextRun).start();
    }

    // passes BigInteger # of solutions to finisher if count succeeds, else null
    public void countSolutions(final ThreadFinisher finisher)
        throws UnavailableOperationException {
        countSolutions(null, finisher);
    }

    public void countSolutions(final Set primaryRelations, final ThreadFinisher finisher)
	throws UnavailableOperationException {
	synchronized(runStatus) {
	    if (!isCountAvailable(primaryRelations != null))
		throw (new UnavailableOperationException());
	    
	    runStatus = COUNT_IN_PROGRESS;
	}

        Runnable countRun = new Runnable() {
            public void run() {
                final Command command = getCommand(); //(Command)commandList.get(commandIndex - 1);
                 BigInteger count;

                try {
                    AlloyRunner.translateCommand(command);
                    count = BigInteger.ZERO;
                    if (true)
                        throw new Error("Solution counting temporarily disabled");
                    //              AlloyRunner.countSolutions(commandData,
                    //                             System.currentTimeMillis(),
                    //                             primaryRelations);
                }
                catch (Exception e) {
                    count = null;
                }

		synchronized(runStatus) {
		    lastRunAborted = isAborting;

		    if (isAborting) {
			count = null;
			isAborting = false;
		    }

		    solutionData = null;
		    solutionCount = 0;
		    lastExecutedCommandInfo = null;
		    
		    runStatus = AVAILABLE;
		}

                finisher.threadFinished(count);
            }
        };

        new Thread(countRun).start();
    }

    public void abort() throws UnavailableOperationException {
	synchronized(runStatus) {
	    if (!isAbortAvailable())
		throw (new UnavailableOperationException());
	    
	    isAborting = true;
	    AlloyRunner.interruptAnalysis();
	}
    }

    public boolean isBuildAvailable() {
        return (runStatus == AVAILABLE);
    }

    public boolean isExecuteAvailable(boolean usePrimaryRelations) {
        return (
            runStatus == AVAILABLE
                && commandIndex != 0
                && (!usePrimaryRelations || enumeratingSolverSelected()));
    }

    public boolean isNextAvailable() {
        try {
            return (
                runStatus == AVAILABLE
                    && getCommandInfo() == getLastExecutedCommandInfo()
                    && solutionData != null
                    && canEnumerate());
        }
        catch (UnavailableOperationException e) {
            return false;
        }
    }

    public boolean isUnsatCoreAvailable() {
	try {
	    return (runStatus == AVAILABLE && 
		    getLastExecutedCommandInfo() != null &&
		    solutionData == null &&
		    unsatCoreSolverSelected());
	} catch (UnavailableOperationException e) {
            return false;
        }
    }

    public boolean isMetamodelAvailable() {
        return (
            runStatus == AVAILABLE
        && areCommandsAvailable());
    }

    public boolean isCountAvailable(boolean usePrimaryRelations) {
        return (
            runStatus == AVAILABLE
                && commandIndex != 0
                && (!usePrimaryRelations || enumeratingSolverSelected())
                && countingSolverSelected());
    }

    public boolean isAbortAvailable() {
        return (runStatus != AVAILABLE);
    }

    public boolean areCommandsAvailable() {
        return (commandList != null);
    }

    // writes model to filePath_
    public void saveModel(String filePath_) throws FileNotFoundException {
        PrintStream toFile = new PrintStream(new FileOutputStream(filePath_));
        toFile.print(spec);
        toFile.close();

        file = new File(filePath_);
    }

    public String getModel() {
        return spec;
    }

    public void setCommand(int i) throws UnavailableOperationException {
        if (!areCommandsAvailable())
            throw (new UnavailableOperationException());

        if (i >= 1 && i <= commandList.size()) {
            commandIndex = i;
        }
    }

    public int getCommandIndex() {
        return commandIndex;
    }

    private Command getCommand() /*throws UnavailableOperationException*/ {
        if (!areCommandsAvailable())
            throw (new RuntimeException(new UnavailableOperationException()));

        return (commandIndex == 0 ? null : (Command)commandList.get(commandIndex - 1));
    }

    /**
     * Returns the Command.Info for the current command.
     * @return null if there are no commands
     * @throws UnavailableOperationException
     */
    public Command.Info getCommandInfo() throws UnavailableOperationException {
    	final Command cmd = getCommand();
    	return cmd==null ? null : cmd.info();
    }

    private Command.Info getLastExecutedCommandInfo() throws UnavailableOperationException {
        if (!areCommandsAvailable())
            throw (new UnavailableOperationException());

        return lastExecutedCommandInfo;
    }

    /** 
     * Returns a list of the Command.Info objects for the Commands.
     * Returning the actually Commands is a potential memory leak.
     * @return
     * @throws UnavailableOperationException
     */
    public List allCommandInfos() throws UnavailableOperationException {
        if (!areCommandsAvailable())
            throw (new UnavailableOperationException());

        final List result = new ArrayList(commandList.size() + 1);
        for (final Iterator i = commandList.iterator(); i.hasNext(); ) {
        		result.add( ((Command)i.next()).info() );
        }
        return Collections.unmodifiableList(result); //commandList;
    }

    public int numCommands() throws UnavailableOperationException {
        if (!areCommandsAvailable())
            throw (new UnavailableOperationException());

        return commandList.size();
    }

    public SolutionData getInstance() {
        return solutionData;
    }

    public int getInstanceNumber() {
        return solutionCount;
    }

    /** remove later... easier for now **/
    public Formula getLastTranslatedFormula() {
	return formulaToAnalyze;
    }

    public LiftedUnsatCore getLiftedUnsatCore() {
	return liftedUnsatCore;
    }

    public RunStatus getRunStatus() {
        return runStatus;
    }

    public boolean lastRunAborted() {
	return lastRunAborted;
    }

    public String getFilePath() {
        return file == null ? null : file.getPath();
    }

    public String getFileName() {
        return file == null ? null : file.getName();
    }

    public boolean canEnumerate() {
        return canEnumerate;
    }

    public boolean enumeratingSolverSelected() {
        return AlloyRunner.enumeratingSolverSelected();
    }

    public boolean countingSolverSelected() {
        return Params.glob.getParam("MAIN", "solver").equalsIgnoreCase("relsat");
    }

    // TODO: not sure which solvers allow for unsat core...
    public boolean unsatCoreSolverSelected() {
	return true;
	//return Params.glob.getParam("MAIN", "solver").equalsIgnoreCase("zchaff");
    }

    /**
     * Evaluates the input string of Alloy over the input solution
     * @param specStr Alloy expression to be evaluated
     * @param solutionData the solution over which the string should be evaluated
     * @return the atom assignment or an error message if <code>specStr</code>
     * is either syntactically or semantically incorrect.
     **/
    public static String evaluateExpr(String specStr_, SolutionData solutionData_) {
        return (new AlloyEvaluator(solutionData_)).evaluate(specStr_);
    }

    /**
     * Evaluates the input string of Alloy over the most
     * recent solution
     * @param specStr Alloy expression to be evaluated
     * @return the atom assignment or an error message if <code>specStr</code>
     * is either syntactically or semantically incorrect.
     **/
    public String evaluateExpr(String specStr_) {
        return evaluateExpr(specStr_, solutionData);
    }

    /** static methods **/

    public static void setOption(String grpName, String paramName, String value) {
        Params.glob.setParam(grpName, paramName, value);
    }

    public static String getOption(String grpName, String paramName) {
        return Params.glob.getParam(grpName, paramName);
    }

    public static String getAllOptions() {
        return Params.glob.toString();
    }

    public static String checkEnvironment() {
        return AlloyRunner.checkEnvironment();
    }

    /** inner classes and interfaces **/

    public interface ThreadFinisher {
        public void threadFinished(Object param);
    }

    private static class RunStatus {
    }
}
